es:ES, e:E, l:IdLnk, L:E List. rcvs from e on l = L  (i:||L||. index(L[i]) = i  ) 

latex

Definitions

||as||, , b, x:AB(x), x:A. B(x), P  Q, False, A, P & Q, AB, i  j < k, , {x:A| B(x) }, {i..j}, x:A. B(x), a<b, #$n, t  T, Void, x:AB(x), es-eq(es), eqof(d), f(a), x.A(x), mu(f), Prop, es_info(es), Id, True, T, ES, IdLnk, A & B, P  Q, rcvs from e on l = L, index(dE;dL;pred?;info;p;r), index(e), l[i], lnk(e), sender(e), es-receives(es;e;l), E, type List, s = t, no_repeats(T;l), x before y  l, P  Q, (e <loc e'), Type

Lemmas

eqof equal btrue, assert wf, mu-bound, le wf, no repeats mu index, es-locl wf, es-locl-antireflexive, no repeats iff, l before wf, int seg wf, es-rcv-from wf, es-rcv-from-equal-receives, select member, es-receives wf, squash wf, true wf, IdLnk wf, event system wf, rcv?-link, rcv?-kind, Id wf, es info wf, mu wf, eqof wf, es-eq wf, select wf, nat wf, length wf1, es-E wf